Adding type support for mutable vs. immutable slices#326
Adding type support for mutable vs. immutable slices#326tahina-pro wants to merge 10 commits intomainfrom
Conversation
| repository: mtzguido/karamel | ||
| ref: dev | ||
| repository: FStarLang/karamel | ||
| ref: _taramana_mutable_slice |
There was a problem hiding this comment.
Oops didn't realize this was still pointing to my repo. When restoring let's just go the main one.
| : Lemma (timeless (pts_to x #p s)) | ||
| [SMTPat (timeless (pts_to x #p s))] | ||
|
|
||
| val from_arrayptr (#t: Type) (a: AP.ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) : stt (ptr t) |
| val base #t (p: ptr t) : GTot (A.array t) | ||
| val offset #t (p: ptr t) : GTot nat | ||
|
|
||
| instance val has_pts_to_array_ptr (t: Type) : has_pts_to (ptr t) (Seq.seq t) |
There was a problem hiding this comment.
We should expose a pts_to function and make this transparent. Otherwise we will get unfolded projectors in the context (at least currently). It would be nice to have exactly this at some point, though.
|
Hi everyone. After releasing EverCBOR, I have some users who want appropriate |
2 participants
tl;dr Breaking changes
If you need mutable slices, you will need to change your code to use
Pulse.Lib.MutableSliceinstead ofPulse.Lib.Slice.Adding type support for mutable vs. immutable slices
With FStarLang/karamel#533, Karamel is on track to supporting F* interfaces implemented in Rust. Thus, mutability analysis requires annotations on the types of such interfaces, to determine which arguments should be
mutand which shouldn't. (@msprotz, please correct me if I'm wrong.)Following a suggestion by @gebner , this PR:
Pulse.Lib.Slice.sliceimmutablePulse.Lib.MutableSlice.slicefor mutable slices (although this wouldn't preclude Karamel's whole-program analysis from refining them as immutable.)To implement immutable slices, I duplicated
Pulse.Lib.ArrayPtrasPulse.Lib.ConstArrayPtrfor const array pointers, which I extract to Cconstpointers. To do so, I rely on type abstraction: supported operations are the same exceptop_Array_Assignmentandcopy, which I removed fromPulse.Lib.ConstArrayPtr.For compatibility purposes, I left interfaces unchanged as much as possible. So, there is a lot of code duplication. Maybe we want a type class for slice operations? I don't know.
I need to:
Pulse.Lib.Sliceto mark them immutable, and add support forPulse.Lib.MutableSlice.